es:ES, p:(E(E + Top)). causal-predecessor(es;p)  (e, e':E. e p< e'  (e < e')) 

latex

Definitions

x:A. B(x), P  Q, t  T, , , A  B, A, False, SQType(T), {T}, p-graph(A;f), f^n, can-apply(f;x), primrec(n;b;c), p-id(), f o g  , do-apply(f;x), Y, if b then t else f fi , (i = j), tt, ff, isl(x), outl(x), Top, A c B, S  T, suptype(S; T), P  Q, T, True, P & Q, P  Q, e p< e', x:A. B(x), , Dec(P), P  Q, causal-predecessor(es;p)

Lemmas

es-p-locl wf, es-E wf, causal-predecessor wf, top wf, event system wf, nat plus properties, p-graph wf2, p-fun-exp wf, le wf, decidable int equal, assert wf, can-apply wf, do-apply wf, es-causl wf, can-apply-fun-exp, squash wf, true wf, bool wf, p-fun-exp-one, p-fun-exp-add, p-compose wf, bnot wf, not wf, bool cases, bool sq, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, es-causl transitivity2, es-causle weakening